es:ES, i:Id, L:(IdLnk List), T:(IdType).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}
es-secret-server(es; T; L; i)
 e@i.
 n:{0..||"table" when e|| }.
 st-atom("table" when e;n) = st-atom("table" when es-init(es;e);n)  Atom1 

latex

Definitions

{T}, SQType(T), (state when e), s.x, Top, True, T, ff, P  Q, P  Q, tt, i  j < k, if b then t else f fi , x. t(x), {i..j}, P & Q, , t  T, secret-table(T), "$x", e@i. P(e), P  Q, Id, x:A. B(x), False, A  B, A, x:A. B(x), @i events of kind k change x to f State(ds) (val:T), xL. P(x), Unit, , x(s), @i(x:T), @i only L affect x:T, A c B, , let x = a in b(x), es-secret-server,

Lemmas

es-loc-init, es-init wf, ss-table-length, st-atom-encrypt, st-length-encrypt, es-val wf, st-encrypt wf, es-kind wf, l member wf, member map, id-deq wf, fpf-cap-single1, rcv wf, Knd wf, map wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, bnot wf, le int wf, le wf, st-atom wf, assert of lt int, eqtt to assert, assert wf, iff transitivity, bool wf, lt int wf, es-constant-1, event system wf, IdLnk wf, Id wf, es-secret-server wf, es-E wf, es-loc wf, st-length wf, data wf, nat wf, secret-table wf, es-vartype wf, es-when wf, int seg wf